T:Type, L1, L2:(T List). fseg(T;L1;L2)  (n:{0..(||L2||+1)}. (L1 = nth_tl(n;L2))) 

latex

ProofTree

Definitions

x:A  B(x), x:A. B(x), Type, type List, as @ bs, s = t, nth_tl(n;as), #$n, ||as||, n+m, {i..j}, t  T, x:AB(x), x:A. B(x), , {x:A| B(x)} , , P  Q, P  Q, P & Q, P  Q, fseg(T;L1;L2), A  B, i  j , a < b, False, A, True, T, , i  j < k, |g|, S  T, [car / cdr], i <z j, i z j, n - m, ff, , b, b, tt, (i = j), x =a y, null(as), a < b, f(a), x f y, a < b, [d], p  q, p  q, p q, Unit, left + right, tl(l), firstn(n;as), Void, {i...j}

Lemmas

append firstn lastn, firstn wf, eqtt to assert, assert of le int, iff transitivity, eqff to assert, bnot of le int, assert of lt int, le int wf, bool wf, lt int wf, assert wf, bnot wf, iff wf, rev implies wf, squash wf, true wf, add functionality wrt eq, length append, length wf nat, nat wf, le wf, non neg length, nth tl wf, int seg wf, length wf1, append wf